#use "hol.ml";;

(* -------------------------------------------------------------------------- *)
(*  Tuples                                                                    *)
(* -------------------------------------------------------------------------- *)



(* -------------------------------------------------------------------------- *)
(*  Concrete Data Types                                                       *)
(* -------------------------------------------------------------------------- *)

type suit = Spades | Hearts | Diamonds | Clubs;;
type suit = Hearts | Spades | Clubs | Diamonds;;

let outranks = function
  | (Spades, Spades) -> false
  | (Spades, _) -> true
  | (Hearts, Spades) -> false
  | (Hearts, Hearts) -> false
  | (Hearts, _) -> true
  | (Diamonds, Clubs) -> true
  | (Diamonds, _) -> false
  | (Clubs, _) -> false;;

type 'a option = None | Some of 'a ;;

let reciprocal = function
  | 0 -> None
  | n -> Some (1 / n);;

match reciprocal 0 with
  | None -> "no recip"
  | Some r -> string_of_int r;;

type 'a llist = Nil | Cons of 'a * 'a llist;;

type 'a tree =
    | Empty 
    | Node of 'a tree * 'a * 'a tree;;

let rec height = function
  | Empty -> 0
  | Node (lft, _, rht) -> 1 + max (height lft) (height rht);;

type 'a tree =
    | Empty 
    | Node of 'a * 'a tree list;;

type 'a tree =
    | Empty 
    | Node of 'a * 'a forest
and 'a forest =
    | None 
    | Tree of 'a tree * 'a forest;;

let rec size_tree = function
  | Empty -> 0
  | Node (_, f) -> 1 + size_forest f
and size_forest = function 
  | None -> 0
  | Tree (t, f') -> size_tree t + size_forest f';;

type 'a tree =
    | Empty 
    | Node of 'a branch * 'a branch
and 'a branch =
    Branch of 'a * 'a tree;;

let rec collect = function 
  | Empty -> []
  | Node (Branch (ld, lt), Branch (rd, rt)) ->
      ld :: rd :: collect lt @ collect rt;;

type expr =
    | Numeral of int 
    | Plus of expr * expr 
    | Times of expr * expr;;

let rec eval = function 
    Numeral n -> Numeral n
  | Plus (e1, e2) ->
      let Numeral n1 = eval e1 in
      let Numeral n2 = eval e2 in
        Numeral (n1+n2)
  | Times (e1, e2) ->
      let Numeral n1 = eval e1 in
      let Numeral n2 = eval e2 in
        Numeral (n1*n2);;

(* -------------------------------------------------------------------------- *)
(*  HOL Light                                                                 *)
(* -------------------------------------------------------------------------- *)

(* 
type term = | Var of string * hol_type
            | Const of string * hol_type
            | Comb of term * term
            | Abs of term * term
*) 

match `1 + 1` with
  | Var _   -> "1 + 1 is a variable"
  | Const _ -> "1 + 1 is a constant"
  | Abs _   -> "1 + 1 is an abstraction"
  | Comb _  -> "1 + 1 is a combination";;

let describe t = 
  let s = string_of_term t in
    match t with
      | Var _   -> s ^ " is a variable"
      | Const _ -> s ^ " is a constant"
      | Abs _   -> s ^ " is an abstraction"
      | Comb _  -> s ^ " is a combination";;

describe `\x. x`;;
